COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	% old definition LTE
C00003 00003	% Measures for OTM operations -- 3-ary
C00006 00004	EVENTS.SINCE(GROUND.ZERO) 2FEB1982
C00010 00005	(SETQ FOO 
C00014 00006	(viii) n ≤< m ∧ m ≤< p -> n ≤< p
C00016 ENDMK
C⊗;
% old definition LTE

DEFN(LTE (X Y) 
    (IF (OZEROP X) T
    (IF (OZEROP Y) F
    (IF (LTE (PA X) (PA Y)) 
	(IF (LTE (PA Y) (PA X)) (LTE (PB X) (PB Y)) (LTE (PB X) Y))
	(IF (LTE (PA Y) (PA X)) (LTE X (PB Y)) F) ))) )

% Measures for OTM operations -- 3-ary

DEFN(OTM.SIZE.3 (X Y Z) (PLUS (COUNT (OFIX X)) (COUNT (OFIX Y)) (COUNT (OFIX Z))))

PROVE.LEMMA(LT.PA.PA.PA (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y)) (NOT (OZEROP Z))
	 (LESSP (OTM.SIZE.3 (PA X) (PA Y) (PA Z)) (OTM.SIZE.3 X Y Z))) )

PROVE.LEMMA(LT.PB.PB.PB (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y)) (NOT (OZEROP Z))
	 (LESSP (OTM.SIZE.3 (PB X) (PB Y) (PB Z)) (OTM.SIZE.3 X Y Z))) )

PROVE.LEMMA(LT.ID.PA.PA (INDUCTION)
(IMPLIES (OR (NOT (OZEROP Y)) (NOT (OZEROP Z))
	 (LESSP (OTM.SIZE.3 X (PA Y) (PA Z)) (OTM.SIZE.3 X Y Z))) )

PROVE.LEMMA(LT.PA.ID.PA (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X))  (NOT (OZEROP Z))
	 (LESSP (OTM.SIZE.3 (PA X) Y (PA Z)) (OTM.SIZE.3 X Y Z))) )

PROVE.LEMMA(LT.PA.PA.ID (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y))
	 (LESSP (OTM.SIZE.3 (PA X) (PA Y) Z) (OTM.SIZE.3 X Y Z))) )

PROVE.LEMMA(LT.ID.PB.PB (INDUCTION)
(IMPLIES (OR (NOT (OZEROP Y)) (NOT (OZEROP Z))
	 (LESSP (OTM.SIZE.3 X (PB Y) (PB Z)) (OTM.SIZE.3 X Y Z))) )

PROVE.LEMMA(LT.PB.ID.PB (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X))  (NOT (OZEROP Z))
	 (LESSP (OTM.SIZE.3 (PB X) Y (PB Z)) (OTM.SIZE.3 X Y Z))) )

PROVE.LEMMA(LT.PB.PB.ID (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y))
	 (LESSP (OTM.SIZE.3 (PB X) (PB Y) Z) (OTM.SIZE.3 X Y Z))) )

EVENTS.SINCE(GROUND.ZERO) 2FEB1982
((BOOT.STRAP) (ADD.SHELL PHI OZERO OTM ((PA (ONE.OF OTM) OZERO) (PB (
ONE.OF OTM) OZERO))) (DEFN OZEROP (X) (OR (EQUAL X (OZERO)) (NOT (OTM X)
))) (DEFN OFIX (X) (IF (OTM X) X (OZERO))) (DEFN OTM.SIZE.2 (X Y) (PLUS 
(COUNT (OFIX X)) (COUNT (OFIX Y)))) (PROVE.LEMMA LT.PB.PB (INDUCTION) (
IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PB X)
 (PB Y)) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PA.PA (INDUCTION) (IMPLIES 
(OR (NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PA X) (PA Y))
 (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PA.PA.x (INDUCTION) (IMPLIES (OR (
NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PA Y) (PA X)) (
OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PB.ID (INDUCTION) (IMPLIES (NOT (
OZEROP X)) (LESSP (OTM.SIZE.2 (PB X) Y) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA
 LT.ID.PB (INDUCTION) (IMPLIES (NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 X (PB
 Y)) (OTM.SIZE.2 X Y)))) (DEFN LTE (X Y) (IF (OZEROP X) T (IF (OZEROP Y)
 F (IF (LTE (PA X) (PA Y)) (IF (LTE (PA Y) (PA X)) (LTE (PB X) (PB Y)) (
LTE (PB X) Y)) (IF (LTE (PA Y) (PA X)) (LTE X (PB Y)) F))))) (DEFN LT (X
 Y) (AND (LTE X Y) (NOT (LTE Y X)))) (DEFN EQ (X Y) (AND (LTE X Y) (LTE 
Y X))) (PROVE.LEMMA LTE.BI (REWRITE) (IMPLIES (NOT (LTE X Y)) (LTE Y X))
) (PROVE.LEMMA LT.PA.ID (INDUCTION) (IMPLIES (NOT (OZEROP X)) (LESSP (
OTM.SIZE.2 (PA X) Y) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.ID.PA (
INDUCTION) (IMPLIES (NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 X (PA Y)) (
OTM.SIZE.2 X Y)))) (PROVE.LEMMA LTE.CASE.LTXY (REWRITE) (IMPLIES (AND (
NOT (OZEROP X)) (NOT (OZEROP Y)) (LT (PA X) (PA Y))) (EQUAL (LTE X Y) (
LTE (PB X) Y)))) (PROVE.LEMMA LTE.CASE.EQXY (REWRITE) (IMPLIES (AND (NOT
 (OZEROP X)) (NOT (OZEROP Y)) (EQ (PA X) (PA Y))) (EQUAL (LTE X Y) (LTE 
(PB X) (PB Y))))) (PROVE.LEMMA LTE.CASE.LTYX (REWRITE) (IMPLIES (AND (
NOT (OZEROP X)) (NOT (OZEROP Y)) (LT (PA Y) (PA X))) (EQUAL (LTE X Y) (
LTE X (PB Y))))) (PROVE.LEMMA LT.CASE.LTXY (REWRITE) (IMPLIES (AND (NOT 
(OZEROP X)) (NOT (OZEROP Y)) (LT (PA X) (PA Y))) (EQUAL (LT X Y) (LT (PB
 X) Y)))) (PROVE.LEMMA LT.CASE.EQXY (REWRITE) (IMPLIES (AND (NOT (OZEROP
 X)) (NOT (OZEROP Y)) (EQ (PA X) (PA Y))) (EQUAL (LT X Y) (LT (PB X) (PB
 Y))))) (PROVE.LEMMA LT.CASE.LTYX (REWRITE) (IMPLIES (AND (NOT (OZEROP X
)) (NOT (OZEROP Y)) (LT (PA Y) (PA X))) (EQUAL (LT X Y) (LT X (PB Y)))))
)
31←
(SETQ FOO 
'((BOOT.STRAP) (ADD.SHELL PHI OZERO OTM ((PA (ONE.OF OTM) OZERO) (PB (
ONE.OF OTM) OZERO))) (DEFN OZEROP (X) (OR (EQUAL X (OZERO)) (NOT (OTM X)
))) (DEFN OFIX (X) (IF (OTM X) X (OZERO))) (DEFN OTM.SIZE.2 (X Y) (PLUS 
(COUNT (OFIX X)) (COUNT (OFIX Y)))) (PROVE.LEMMA LT.PB.PB (INDUCTION) (
IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PB X)
 (PB Y)) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PB.PB.x (INDUCTION) (
IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PB Y)
 (PB X)) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PA.PA (INDUCTION) (IMPLIES 
(OR (NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PA X) (PA Y))
 (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PA.PA.x (INDUCTION) (IMPLIES (OR (
NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PA Y) (PA X)) (
OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PA.ID (INDUCTION) (IMPLIES (NOT (
OZEROP X)) (LESSP (OTM.SIZE.2 (PA X) Y) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA
 LT.PA.ID.x (INDUCTION) (IMPLIES (NOT (OZEROP X)) (LESSP (OTM.SIZE.2 Y (
PA X)) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PB.ID (INDUCTION) (IMPLIES (
NOT (OZEROP X)) (LESSP (OTM.SIZE.2 (PB X) Y) (OTM.SIZE.2 X Y)))) (
PROVE.LEMMA LT.PB.ID.x (INDUCTION) (IMPLIES (NOT (OZEROP X)) (LESSP (
OTM.SIZE.2 Y (PB X)) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.ID.PA (
INDUCTION) (IMPLIES (NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 X (PA Y)) (
OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.ID.PA.x (INDUCTION) (IMPLIES (NOT (
OZEROP Y)) (LESSP (OTM.SIZE.2 (PA Y) X) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA
 LT.ID.PB (INDUCTION) (IMPLIES (NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 X (PB
 Y)) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.ID.PB.x (INDUCTION) (IMPLIES (
NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 (PB Y) X) (OTM.SIZE.2 X Y)))) (DEFN 
LTE (X Y) (IF (OZEROP X) T (IF (OZEROP Y) F (OR (AND (LTE (PA X) (PA Y))
 (NOT (LTE (PA Y) (PA X))) (LTE (PB X) Y)) (AND (LTE (PA X) (PA Y)) (LTE
 (PA Y) (PA X)) (LTE (PB X) (PB Y))) (AND (NOT (LTE (PA X) (PA Y))) (LTE
 (PA Y) (PA X)) (LTE X (PB Y))))))) (PROVE.LEMMA OZERO.LTE.X NIL (LTE (
OZERO) X)) (PROVE.LEMMA X.LTE.OZERO NIL (IMPLIES (AND (OZEROP Y) (LTE X 
Y)) (OZEROP X))) (DEFN LTE1 (X) (IF (OZEROP X) T (AND (LTE1 (PA X)) (
LTE1 (PB X))))) (PROVE.LEMMA LTE.XX (REWRITE) (EQUAL (LTE X X) (LTE1 X))
) (PROVE.LEMMA REFLEX.LTE NIL (LTE X X)) (PROVE.LEMMA TOTAL.LTE NIL (
IMPLIES (NOT (LTE X Y)) (LTE Y X)))) )

(viii) n ≤< m ∧ m ≤< p -> n ≤< p
PROVE.LEMMA(TRANS.LTE NIL (IMPLIES (AND (LTE X Y) (LTE Y Z)) (LTE X Z)) )
TRANS.LTE 0=0 Running at 330315  Used 0:16:41.7 in 0:51:38, Load   1.04
 0=0 Running at 1003  Used 0:17:21.2 in 0:52:20, Load   1.03
 0=0 Running at 12037  Used 0:18:21.7 in 0:53:24, Load   1.02
 0=0 Running at 315763  Used 0:21:08.4 in 0:56:21, Load   1.05
 0=0 Running at 25077  Used 08εr:35.4 in 0:57:53, Load   1.02
 0=0 Running at 25077  Used 0:26:58.0 in 1:02:31, Load   1.02
***ERROR***

STORAGE FULL
 0=0 Running at 30530  Used 0:28:02.0 in 1:03:38, Load   1.02
NIL

   (ALL.PICKS broken)
11:




PROVE.LEMMA(TRANS.LTE NIL (IMPLIES (AND (LTE X Y) (LTE Y Z)) (LTE X Z)) )			
PROVE.LEMMA(TRANS1.LTE NIL 
    (IMPLIES (AND (NOT (LTE X Z)) (LTE Y Z)) (NOT (LTE X Y))) )			
PROVE.LEMMA(TRANS2.LTE NIL 
    (IMPLIES (AND (LTE X Y) (NOT (LTE X Z))) (NOT (LTE Y Z))) )